module DAG

sig Graph {
	nodes: set Node
}

sig Node {
	neighbors: set Node
}

// All Nodes this Node is a neighbor of
//fun parents [n: Node]: set Node {
	//supposed to return Node minus all nodes that don't have n in neighbors
//}

fact Acyclic {
	all n: Node | no n & n.^neighbors
}

// All Nodes are members of a Graph
fact Membership {
	all n: Node | some g: Graph | n in g.nodes
}

// No nodes are a member of multiple graphs or connected to the nodes of other graphs
fact Separation {
	all disj g, h: Graph | no g.nodes & h.nodes
	all g: Graph | g.nodes.^neighbors in g.nodes
	//once fun parents works, hopefully can replace last line with:  
	//	all g: Graph, n: Node | n in g.nodes implies parents[n] in g.nodes
}

// At least one source (no incoming edges)
assert Source {
	all g: Graph | some n: Node | n in g.nodes and no n & Node.neighbors
}

// At least one sink (no outgoing edges)
assert Sink {
	all g: Graph | some n: Node | n in g.nodes and no n.neighbors
}

pred addNode [g, g': Graph, n: Node] {
	g'.nodes = g.nodes + n
}

pred addEdge [g, g': Graph, n, n': Node] {
	(g'.nodes & n).neighbors = (g.nodes & n).neighbors + n'
}

// remove node and all incoming edges
pred delNode [g, g': Graph, n: Node] {
	g'.nodes = g.nodes - n
	g'.nodes.neighbors = g.nodes.neighbors - n
}

// remove an edge from a graph
pred delEdge [g, g': Graph, n, n': Node] {
	(g'.nodes & n).neighbors = (g.nodes & n).neighbors - n'
}

// Adding a node (not previously in the graph) and deleting it results in the same graph
assert delNodeUndoesAddNode {
	all g, g', g'': Graph, n: Node |
		no n & g.nodes and addNode [g, g', n] and delNode [g', g'', n]
		implies
		g.nodes = g''.nodes
}

assert delNodeUndoesAddNodeAndAddEdge {
	all g, g', g'',g''': Graph, n, n': Node |
		no n & g.nodes and n' in g.nodes and addNode [g, g', n] and addEdge [g', g'', n', n] and delNode [g'', g''', n]
		implies
		g.nodes = g'''.nodes
}

// Adding an edge (not previously in the graph) and deleting it results in the same graph
assert delEdgeUndoesAddEdge {
	all g, g', g'': Graph, n, n': Node |
		no n' & n.neighbors and addEdge[g, g', n, n'] and delEdge[g', g'', n, n']
		implies
		(g.nodes & n).neighbors = (g''.nodes & n).neighbors
}

//check delNodeUndoesAddNode for 8

//check delNodeUndoesAddNodeAndAddEdge for 8

//check delEdgeUndoesAddEdge for 8

pred prettyGraph {
	#Graph > 1
	all g: Graph | #g.nodes > 3
	#Node.neighbors.neighbors > 2
}


run prettyGraph for 20
